(assert (= "bZAHP6GSLAbZAHP6GSLAbZAHP6GSLAbZAHP6GSLA" (str.replace_all "bZAHP6GSLAbZAHP6GSLA" "bZAHP6GSLA" "bZAHP6GSLAbZAHP6GSLA")))
(check-sat)
